> import Data.List
> import Lib.Logic
> import Lib.Set
> import Lib.BinaryRelation

A legfontosabb fogalmak:

1. állapottér		A = (A1, A2, ... An)
2. feladat			F ⊆ A × A
3. program			S ⊆ A × A**
4. programfüggvény  p(S) ⊆ A × A
5. megoldás			

Megjegyzések:

A × A   <=> [(a,a)]
A × A** <=> [(a,[a])]

Példa állapottér

> al1 = [1,2,3,4,5]

Példa feladat

> f1 = [(2,1),(3,4)]

Példák programra

> s1 = [(2,[2,1,2,1]++[2,2..]),(2,[3,4,5])]
> s2 = [(2,[2,3,4,1]),(3,[3,5,4])]

Eldöntése annak, hogy program-e az adott program

Ellenőrizendő feltételek:
  1. ?? DS = A,
  2. OK ∀α ∈ RS : α = red(α),
  3. OK ∀a ∈ A : ∀α ∈ S(a) : |α| = 0 és α1 = a.

> programE :: (Eq a) => [(a,[a])] -> Bool
> programE a = and (map f a) where
>   f :: (Eq a) => (a,[a]) -> Bool
>   f (a,[])   = False
>   f (a,x:xs) = (a == x) && red(x:xs) == (x:xs)

Megadja a program értelmezési tartományát

mivel a program egy reláció:
Lib.BinaryRelation.domain

Megadja a program érték készletét

mivel a program egy reláció:
Lib.BinaryRelation.range

Redukálja az adott sorozatot

> red :: (Eq a) => [a] -> [a]
> red [] = []
> red [b] = [b]
> red (b1:b2:bs)
>   | b1 == b2  = red (b2:bs)
>   | otherwise = b1:red(b2:bs)
 
Átalakítja a programot programfüggvénnyé

Ellenőrizendő feltételek:
  1. ?? Dp(S) = {a ∈ A | S(a) ⊆ A∗ },
  2. OK p(S)(a) = {b ∈ A | ∃α ∈ S(a) : τ (α) = b}.

> programFuggveny :: [(a,[a])] -> [(a,a)]
> programFuggveny a =  {-filter g-} (map f a) where
>   f :: (a,[a]) -> (a,a)
>   f (a,b) = (a,last b)
>   --g :: (a,a) -> Bool
>   --g (a,b) = elem a vegtelenSorozat x

[Komment kell még ide]

> vegtelenSorozat :: (Eq a) => [(a,[a])] -> [a]
> vegtelenSorozat a = nub (map (\(b,c)->b) (filter (not.f) a)) where
>   f :: (Eq a) => (a,[a]) -> Bool
>   f (a,[]) = True
>   f (a,[b]) = True
>   f (a,b1:b2:bs) = (b1 /= b2) && f (a,b2:bs)

Megoldja-e az adott programfüggvény az adott feladatot?
MegoldjaE :: Program -> Feladat -> Bool

Azt mondjuk, hogy az S program megoldja az F feladatot, ha
  1. DF ⊆ Dp(S) ,
  2. ∀a ∈ DF : p(S)(a) ⊆ F(a).

> megoldjaE :: (Eq a) => [(a,[a])] -> [(a,a)] -> Bool
> megoldjaE s f = (df ⊆ dpS) && (all (\a -> (imgMem pS a) ⊆ (imgMem f a)) df) where
>   df = domain f
>   dpS = domain pS
>   pS = programFuggveny s